#include "atom.h"
#include "bind.h"
#include "predicates.h"
#include "prover.h"
#include "system.h"
#include "tree.h"
#include "tuple.h"

class ascii : public OnceBindTupleProver {
predicateName("ascii")

  bool proveOnce () {
    Node &charNode = *tuple->nodes[1].final ();
    Node &valueNode = *tuple->nodes[2].final ();
    char type;
    switch(valueNode.type ()) {
    case Reference::ID:
      type = charNode.type ();
      return (type == Atom::ID || type == String::ID) && binder.bind (
          valueNode, *Number::create (
              (unsigned char) static_cast<Atom&> (charNode).name[0]),
          system->trail);
    case Number::ID:
      return binder.bind (charNode, *new String (std::string (1,
          static_cast<Number&> (valueNode).value)), system->trail);
    default:
      return false;
    }
  }
};

ProverFactoryRegistrar<ascii, Tuple::ID, 3> asciiRegistrar;

class compare : public OnceProver {
predicateName("compare")

  bool proveOnce () {
    return compareNodes (*tuple->nodes[1].final (), *tuple->nodes[2].final ())
        < 0;
  }

  Tuple *tuple;
  void set (Tuple &t, System&) {
    tuple = &t;
  }
};

ProverFactoryRegistrar<compare, Tuple::ID, 3> compareRegistrar;

class concat : public OnceBindTupleProver {
predicateName("concat")

  bool proveOnce () {
    std::string result;
    for(std::vector<pNode>::iterator pi = tuple->nodes.begin () + 1; pi
        < tuple->nodes.end () - 1; pi++)
      result += pi->display ();

    bool ret = binder.bind (**(tuple->nodes.end () - 1), *new String (result),
        system->trail);
    return ret;
  }
};

ProverFactoryRegistrar<concat, Tuple::ID> concatRegistrar;

class LengthSwitcher : public Switcher {
public:
  bool atom (Atom &a) {
    length = a.name.length ();
    return true;
  }

  bool tuple (Tuple &t) {
    length = t.nodes.size ();
    return true;
  }

  std::string::size_type length;
};

// Returns -1 if the type has no definition of length
int lengthOf (Node &node) {
  LengthSwitcher lengthSwitcher;
  return node.doSwitch (lengthSwitcher) ? (int) lengthSwitcher.length : -1;
}

class length : public Prover {
predicateName("length")

  bool prove () {
    if(!tuple) { // Fail any backtrack
      binder.undo (system->trail);
      return false;
    } else
      binder.capture (system->trail);

    pNode resultNode;
    bool ret;
    int length = lengthOf (*tuple->nodes[1]);
    if(length >= 0)
      ret = binder.bind (*tuple->nodes[2], *Number::create (length),
          system->trail);

    // Length -1 means input unbounded; creates a tuple of unbinded elements
    else {
      Node &countNode = *tuple->nodes[2].final ();
      if(countNode.type () == Number::ID) {
        int n = static_cast<Number&> (countNode).value;

        Tuple *list = new Tuple;
        list->nodes.reserve (n);
        for(int i = 0; i < n; i++)
          list->nodes.push_back (new Reference);

        ret = binder.bind (*tuple->nodes[1], *list, system->trail);
      } else
        return false; // Hardly too much freedom...
    }

    tuple = 0;
    return ret;
  }

  Binder binder;
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<length, Tuple::ID, 3> lengthRegistrar;

class mnth : public OnceBindTupleProver {
predicateName("mnth")

  class ContainerSwitcher : public Switcher {
  public:
    ContainerSwitcher (int l, int r) :
      left (l), right (r) {
    }

    bool atom (Atom &a) {
      element = new String (a.name.substr (left, right - left));
      return true;
    }

    bool tuple (Tuple &t) {
      Tuple *newTuple = new Tuple;
      for(int i = left; i < right; i++)
        newTuple->nodes.push_back (t.nodes[i]);
      element = newTuple;
      return true;
    }
    int left, right;
    pNode element;
  };

  // Warning: no bounds checking!
  bool proveOnce () {
    Tuple &container = static_cast<Tuple&> (*tuple->nodes[1].final ());
    int left = static_cast<Number&> (*tuple->nodes[2].final ()).value;
    int right = static_cast<Number&> (*tuple->nodes[3].final ()).value;
    int length = lengthOf (container);

    if(length > 0) {
      if(left < 0)
        left += length;
      if(right <= 0)
        right += length;
    } else
      left = right = 0;

    Tuple *newTuple = new Tuple;
    for(int i = left; i < right; i++)
      newTuple->nodes.push_back (container.nodes[i]);

    return binder.bind (*tuple->nodes[4], *newTuple, system->trail);
  }

};

ProverFactoryRegistrar<mnth, Tuple::ID, 5> mnthRegistrar;

class nth : public Prover {
predicateName("nth")

  class ContainerSwitcher : public Switcher {
  public:
    ContainerSwitcher (int i) :
      index (i) {
    }

    bool atom (Atom &a) {
      if(index < 0)
        index += a.name.length ();
      element = new String (a.name.substr (index, 1));
      return true;
    }

    bool tree (Tree &t) {
      if(index == 0)
        element = new String (t.ops[1] ? std::string (t.ops, 2) : std::string (
            t.ops));
      else if(index == -1)
        element = t.left;
      else if(index == 1)
        element = t.right;
      else
        return false;
      return true;
    }

    bool tuple (Tuple &t) {
      if(index < 0)
        index += t.nodes.size ();
      element = t.nodes[index];
      return true;
    }

    int index;
    pNode element;
  };

  // Warning: no bounds checking!
  bool prove () {
    reProve: if(state)
      binder.undo (system->trail); // Undoes previous bind
    else
      binder.capture (system->trail);
    if(state < 0)
      return false; // I shall succeed no more

    Node &container = *tuple->nodes[1].final ();
    Node &indexNode = *tuple->nodes[2].final ();
    int index;

    switch(indexNode.type ()) {
    case Reference::ID:
      if(state >= lengthOf (container))
        return false;
      else
        binder.bind (indexNode, // True assumed
            *Number::create (index = state++), system->trail);
      break;
    case Number::ID:
      index = static_cast<Number&> (indexNode).value;
      state = -1; // No backtrack
      break;
    default:
      return false;
    }

    ContainerSwitcher containerSwitcher (index);
    if(container.doSwitch (containerSwitcher))
      if(binder.bind (*tuple->nodes[3], *containerSwitcher.element,
          system->trail))
        return true;
      else
        goto reProve;
    else
      return false;
  }

  int state;
  Binder binder;
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    state = 0;
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<nth, Tuple::ID, 4> nthRegistrar;

class parse : public OnceBindTupleProver {
predicateName("parse")

  bool proveOnce () {
    return binder.bind (*tuple->nodes[2], *Node::parse (
        tuple->nodes[1].node->display ()), system->trail);
  }
};

ProverFactoryRegistrar<parse, Tuple::ID, 3> parseRegistrar;

class substr : public OnceBindTupleProver {
predicateName("substr")

  // Warning: no bounds checking!
  bool proveOnce () {
    Node &container = *tuple->nodes[1].final ();
    Node &leftNode = *tuple->nodes[2].final ();
    Node &rightNode = *tuple->nodes[3].final ();

    if(typeid(container) != typeid(Atom) &&
        typeid(container) != typeid(String))
      return false;
    std::string &s = static_cast<Atom&> (container).name;

    if(typeid(leftNode) != typeid(Number) ||
        typeid(rightNode) != typeid(Number)) {
      Node &matchNode = static_cast<String&> (*tuple->nodes[4].final ());
      if(typeid(matchNode) != typeid(String))
        return false;

      std::string &toMatch = static_cast<String&> (matchNode).name;
      std::string::size_type pos = s.find (toMatch);

      return pos != std::string::npos &&
        binder.bind (leftNode, *Number::create (pos), system->trail) &&
        binder.bind (rightNode, *Number::create (pos + toMatch.length ()),
          system->trail);
    }

    int left = static_cast<Number&> (leftNode).value;
    int right = static_cast<Number&> (rightNode).value;
    int length = s.length ();

    if(length > 0) {
      if(left < 0)
        left += length;
      if(right <= 0)
        right += length;
    } else
      left = right = 0;

    return binder.bind (
        *tuple->nodes[4], *new String (s.substr (left, right - left)),
        system->trail);
  }

};

ProverFactoryRegistrar<substr, Tuple::ID, 5> substrRegistrar;
